Termination Proof Script

• Consider the SCC {20-30,32,33}. By taking the AF π with π(a__from) = π(A__FROM) = π(cons) = π(from) = π(mark) = π(MARK) = 1, π(A__ADD) = π(A__FST) = 2 and π(s) = [ ] together with the lexicographic path order with precedence a__len ≻ 0 ≻ nil, a__len ≻ s, a__fst ≈ fst, a__add ≈ add and a__len ≈ len, the rules in {3,8-22,26,27,33} are weakly decreasing and the rules in {1,2,4-7,23-25,28-30,32} are strictly decreasing. There is one new SCC.
  • Consider the SCC {21,26,27,33}. By taking the AF π with π(A__FROM) = π(cons) = π(mark) = π(MARK) = π(s) = 1, π(a__add) = π(add) = 2, π(a__len) = π(len) = [ ] and π(a__fst) = π(fst) = [2] together with the lexicographic path order with precedence a__fst ≻ nil, a__len ≻ 0, a__fst ≈ fst, a__from ≈ from and a__len ≈ len, the rules in {4,5,7-19,21,33} are weakly decreasing and the rules in {1-3,6,26,27} are strictly decreasing. There is one new SCC.
    • Consider the SCC {33}. There are no usable rules. By taking the AF π with π(MARK) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 33 is strictly decreasing.